Inference at * 1 
Iof proof for Lemma l before antisymmetry:



1. T : Type
2. l : T List
3. x : T
4. y : T
5. no_repeats(T;l)
6. [x; y]  l
7. [y; x]  l
  False 

latex

 by Assert [x; x]  l 

latex

 1: .....assertion..... NILNIL

 1:   [x; x]  l
 2: 

 2: 8. [x; x]  l
 2:   False
 .

Definitions

L1  L2, [car / cdr], []